back to root

back to Matryoshka

Problem SEU868^5

• Petar Vukmirovic

  2020-05-04 11:52:11 (GMT)

  I have been reading the Satallax paper, and there is a very intersting example in there (SEU868^5)

• Petar Vukmirovic

  2020-05-04 11:52:24 (GMT)

  The only way to solve in Zip is using lambda-lifting and letting Ehoh solve it

• Petar Vukmirovic

  2020-05-04 11:53:27 (GMT)

  After looking at the proof for some time I had :light_bulb: moment. Namely, Variables in two clauses need to be instantiated with $\lambda x. t$ where $t$ is one relatively complex formula.

• Petar Vukmirovic

  2020-05-04 11:53:50 (GMT)

  And when that is done, there is still a looot of inferences that are possible and Zip gets completely lost

• Jasmin Blanchette

  2020-05-04 11:55:2 (GMT)

  $f$ and $g$ are not ideal letters for formulas. Most people write $\phi, \psi$ (including Wan in Logic and Sets). $f$ and $g$ look like function symbols (most authors wouldn't use \mathsf there).

• Petar Vukmirovic

  2020-05-04 11:55:31 (GMT)

  Then I realized that this variable will never get instantiated with the needed term through superpostion normally... BUT if you name the lambda, suddently there is going to be a function symbol of the appropriate kind that can be superposed from, and the needed inference is going to be performed

• Jasmin Blanchette

  2020-05-04 11:56:1 (GMT)

  (Oops wrong thread.)

• Petar Vukmirovic

  2020-05-04 11:56:42 (GMT)

  Making Zip (and Ehoh) behave like tableaux prover in the sense that they will instantiate with wanted lambda

• Petar Vukmirovic

  2020-05-04 11:57:29 (GMT)

  All this to say that now I believe more strongly that Satallax should not be so easily written off and has some real advantages in higher-order proving

• Petar Vukmirovic

  2020-05-04 11:57:53 (GMT)

  I have compiled a list of 3 things that we could do to make Zip behave a bit more like Satallax in some case

• Jasmin Blanchette

  2020-05-04 11:57:55 (GMT)

  Rule ExtER will infer

  That an inference rule should infer something sounds strange. Maybe "produce" or "generate" (cf. "generating inferences").

• Petar Vukmirovic

  2020-05-04 12:25:54 (GMT)

  @Alexander Bentkamp : We can discuss them on Thursday

• Jasmin Blanchette

  2020-05-04 12:27:16 (GMT)

  Is Alex taking a 3-day vacation without my permission? ;)

• Simon Cruanes

  2020-05-04 19:25:52 (GMT)

  @Petar Vukmirovic and how hard is SYO548ˆ1 for Zipper/Ehoh?

• Petar Vukmirovic

  2020-05-04 19:37:28 (GMT)

  solvable :slight_smile:

• Simon Cruanes

  2020-05-04 19:37:51 (GMT)

  Nice. Could you post the graph of the proof? :)

• Petar Vukmirovic

  2020-05-04 19:39:33 (GMT)

  image.png

  

• Petar Vukmirovic

  2020-05-04 19:39:37 (GMT)

  Solved in 0s

• Simon Cruanes

  2020-05-04 19:42:31 (GMT)

  That's quite impressive. I also realize how out of touch I am these days with Zipperposition's rules, because inst_choice looks like magic to me!

• Petar Vukmirovic

  2020-05-05 10:34:3 (GMT)

  Thanks :slight_smile:

  What I think really makes this example interesting is the need for complicated HO unification and instantiation with the negation of a choice trigger